0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 20 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 3 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 104 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
TRANSPOSE_IN_AG(A, B) → U1_AG(A, B, transpose_aux_in_agg(A, nil, B))
TRANSPOSE_IN_AG(A, B) → TRANSPOSE_AUX_IN_AGG(A, nil, B)
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → ROW2COL_IN_AGAA(R, cons(C, Cs), Cols1, Accm)
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_AGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_AGG(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
TRANSPOSE_IN_AG(A, B) → U1_AG(A, B, transpose_aux_in_agg(A, nil, B))
TRANSPOSE_IN_AG(A, B) → TRANSPOSE_AUX_IN_AGG(A, nil, B)
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → ROW2COL_IN_AGAA(R, cons(C, Cs), Cols1, Accm)
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_AGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_AGG(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
ROW2COL_IN_AGAA(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
ROW2COL_IN_AGAA(cons(cons(X, Ys), Cols)) → ROW2COL_IN_AGAA(Cols)
From the DPs we obtained the following set of size-change graphs:
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, nil, B))
transpose_aux_in_agg(cons(R, Rs), X1, cons(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg(nil, X, X) → transpose_aux_out_agg(nil, X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(cons(R, Rs), X1, cons(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, nil, B)) → transpose_out_ag(A, B)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, cons(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(cons(R, Rs), X1, cons(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, cons(C, Cs), Cols1, Accm))
row2col_in_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(cons(X, Ys), Cols), cons(Ys, Cols1), cons(nil, As))
row2col_in_agaa(nil, nil, nil, nil) → row2col_out_agaa(nil, nil, nil, nil)
U2_AGG(row2col_out_agaa(R, Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(X1, cons(C, Cs)) → U2_AGG(row2col_in_agaa(cons(C, Cs)))
row2col_in_agaa(cons(cons(X, Ys), Cols)) → U4_agaa(X, Ys, row2col_in_agaa(Cols))
U4_agaa(X, Ys, row2col_out_agaa(Xs, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(Ys, Cols1), cons(nil, As))
row2col_in_agaa(nil) → row2col_out_agaa(nil, nil, nil)
row2col_in_agaa(x0)
U4_agaa(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U2_AGG(row2col_out_agaa(R, Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Accm, Cols1)
POL( U2_AGG(x1) ) = x1 + 2
POL( row2col_in_agaa(x1) ) = max{0, 2x1 - 2}
POL( cons(x1, x2) ) = x1 + x2 + 1
POL( U4_agaa(x1, ..., x3) ) = 2x1 + 2x2 + x3 + 2
POL( nil ) = 0
POL( row2col_out_agaa(x1, ..., x3) ) = max{0, 2x2 - 1}
POL( TRANSPOSE_AUX_IN_AGG(x1, x2) ) = 2x2
row2col_in_agaa(cons(cons(X, Ys), Cols)) → U4_agaa(X, Ys, row2col_in_agaa(Cols))
row2col_in_agaa(nil) → row2col_out_agaa(nil, nil, nil)
U4_agaa(X, Ys, row2col_out_agaa(Xs, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(Ys, Cols1), cons(nil, As))
TRANSPOSE_AUX_IN_AGG(X1, cons(C, Cs)) → U2_AGG(row2col_in_agaa(cons(C, Cs)))
row2col_in_agaa(cons(cons(X, Ys), Cols)) → U4_agaa(X, Ys, row2col_in_agaa(Cols))
U4_agaa(X, Ys, row2col_out_agaa(Xs, Cols1, As)) → row2col_out_agaa(cons(X, Xs), cons(Ys, Cols1), cons(nil, As))
row2col_in_agaa(nil) → row2col_out_agaa(nil, nil, nil)
row2col_in_agaa(x0)
U4_agaa(x0, x1, x2)